/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Yury Kudryashov, Kim Morrison
-/
import Mathlib.Data.Finsupp.SMul

/-!
# Monoid algebras

When the domain of a `Finsupp` has a multiplicative or additive structure, we can define
a convolution product. To mathematicians this structure is known as the "monoid algebra",
i.e. the finite formal linear combinations over a given semiring of elements of the monoid.
The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.

In fact the construction of the "monoid algebra" makes sense when `G` is not even a monoid, but
merely a magma, i.e., when `G` carries a multiplication which is not required to satisfy any
conditions at all. In this case the construction yields a not-necessarily-unital,
not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such
algebras to magmas, and we prove this as `MonoidAlgebra.liftMagma`.

In this file we define `MonoidAlgebra k G := G →₀ k`, and `AddMonoidAlgebra k G`
in the same way, and then define the convolution product on these.

When the domain is additive, this is used to define polynomials:
```
Polynomial R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)
```

When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

## Notation

We introduce the notation `R[A]` for `AddMonoidAlgebra R A`.

## Implementation note
Unfortunately because additive and multiplicative structures both appear in both cases,
it doesn't appear to be possible to make much use of `to_additive`, and we just settle for
saying everything twice.

Similarly, I attempted to just define
`k[G] := MonoidAlgebra k (Multiplicative G)`, but the definitional equality
`Multiplicative G = G` leaks through everywhere, and seems impossible to use.
-/

assert_not_exists NonUnitalAlgHom AlgEquiv

noncomputable section

open Finsupp hiding single

universe u₁ u₂ u₃ u₄

variable (k : Type u₁) (G : Type u₂) (H : Type*) {R S M : Type*}

/-! ### Multiplicative monoids -/


section

variable [Semiring k]

/-- The monoid algebra over a semiring `k` generated by the monoid `G`.
It is the type of finite formal `k`-linear combinations of terms of `G`,
endowed with the convolution product.
-/
@[to_additive (relevant_arg := 2) /--
The monoid algebra over a semiring `k` generated by the additive monoid `G`, denoted by `k[G]`.
It is the type of finite formal `k`-linear combinations of terms of `G`,
endowed with the convolution product. -/, to_additive_dont_translate]
def MonoidAlgebra : Type max u₁ u₂ :=
  G →₀ k

namespace AddMonoidAlgebra

@[inherit_doc AddMonoidAlgebra]
scoped syntax:max (priority := high) term noWs "[" term "]" : term

macro_rules | `($k[$g]) => `(AddMonoidAlgebra $k $g)

/-- Unexpander for `AddMonoidAlgebra`. -/
@[scoped app_unexpander AddMonoidAlgebra]
def unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $k $g) => `($k[$g])
  | _ => throw ()

end AddMonoidAlgebra

@[to_additive]
instance MonoidAlgebra.inhabited : Inhabited (MonoidAlgebra k G) :=
  inferInstanceAs (Inhabited (G →₀ k))

@[to_additive AddMonoidAlgebra.addCommMonoid]
instance MonoidAlgebra.addCommMonoid : AddCommMonoid (MonoidAlgebra k G) :=
  inferInstanceAs (AddCommMonoid (G →₀ k))

@[to_additive]
instance MonoidAlgebra.instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (MonoidAlgebra k G) :=
  inferInstanceAs (IsCancelAdd (G →₀ k))

@[to_additive]
instance MonoidAlgebra.coeFun : CoeFun (MonoidAlgebra k G) fun _ => G → k :=
  inferInstanceAs (CoeFun (G →₀ k) _)

end

namespace MonoidAlgebra

variable {k G}

section

variable [Semiring k] [NonUnitalNonAssocSemiring R]

-- TODO: This definition is very leaky, and we later have frequent problems conflating the two
-- versions of `single`. Perhaps someone wants to try making this a `def` rather than an `abbrev`?
-- In Mathlib 3 this was locally reducible.
/-- `MonoidAlgebra.single a r` for `a : M`, `r : R` is the element `ar : R[M]`. -/
@[to_additive /-- `AddMonoidAlgebra.single a r` for `a : M`, `r : R` is the element `ar : R[M]`. -/]
abbrev single (a : G) (b : k) : MonoidAlgebra k G := Finsupp.single a b

@[to_additive]
theorem single_zero (a : G) : (single a 0 : MonoidAlgebra k G) = 0 := Finsupp.single_zero a

@[to_additive]
theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
  Finsupp.single_add a b₁ b₂

@[to_additive]
theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
    (h_zero : h a 0 = 0) :
    (single a b).sum h = h a b := by
  simp [h_zero]

@[to_additive (attr := simp)]
theorem sum_single (f : MonoidAlgebra k G) : f.sum single = f :=
  Finsupp.sum_single f

@[to_additive]
theorem single_apply {a a' : G} {b : k} [Decidable (a = a')] :
    single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

@[to_additive (attr := simp)]
theorem single_eq_zero {a : G} {b : k} : single a b = 0 ↔ b = 0 := Finsupp.single_eq_zero

@[to_additive]
theorem single_ne_zero {a : G} {b : k} : single a b ≠ 0 ↔ b ≠ 0 := Finsupp.single_ne_zero

@[to_additive (attr := elab_as_elim)]
lemma induction_linear {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G) (zero : p 0)
    (add : ∀ f g : MonoidAlgebra k G, p f → p g → p (f + g)) (single : ∀ a b, p (single a b)) :
    p f := Finsupp.induction_linear f zero add single

end

section Mul

variable [Semiring k] [Mul G]

/-- The multiplication in a monoid algebra. We make it irreducible so that Lean doesn't unfold
it trying to unify two things that are different. -/
@[irreducible] def mul' (f g : MonoidAlgebra k G) : MonoidAlgebra k G :=
  f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)

/-- The product of `f g : MonoidAlgebra k G` is the finitely supported function
whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
such that `x * y = a`. (Think of the group ring of a group.) -/
instance instMul : Mul (MonoidAlgebra k G) := ⟨MonoidAlgebra.mul'⟩

/-- The product of `f g : k[G]` is the finitely supported function
whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
such that `x + y = a`. (Think of the product of multivariate
polynomials where `α` is the additive monoid of monomial exponents.) -/
instance _root_.AddMonoidAlgebra.instMul [Add G] : Mul (AddMonoidAlgebra k G) :=
  ⟨fun f g => MonoidAlgebra.mul' (G := Multiplicative G) f g⟩

attribute [to_additive existing instMul] instMul

@[to_additive (dont_translate := k) mul_def]
theorem mul_def {f g : MonoidAlgebra k G} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂) := by
  with_unfolding_all rfl

@[to_additive (dont_translate := k)]
instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (MonoidAlgebra k G) :=
  { Finsupp.instAddCommMonoid with
    -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
    left_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
        simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
    right_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
        simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]
    zero_mul := fun f => by
      simp only [mul_def]
      exact sum_zero_index
    mul_zero := fun f => by
      simp only [mul_def]
      exact Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_zero_index)) sum_zero }

end Mul

section Semigroup

variable [Semiring k] [Semigroup G] [Semiring R]

@[to_additive (dont_translate := k)]
instance nonUnitalSemiring : NonUnitalSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalNonAssocSemiring with
    mul_assoc := fun f g h => by
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [mul_def]
      rw [sum_sum_index] <;> congr; on_goal 1 => ext a₁ b₁
      rw [sum_sum_index, sum_sum_index] <;> congr; on_goal 1 => ext a₂ b₂
      rw [sum_sum_index, sum_single_index] <;> congr; on_goal 1 => ext a₃ b₃
      on_goal 1 => rw [sum_single_index, mul_assoc, mul_assoc]
      all_goals simp only [single_zero, single_add, forall_true_iff, add_mul,
        mul_add, zero_mul, mul_zero, sum_zero, sum_add] }

end Semigroup

section One

variable [NonAssocSemiring R] [Semiring k] [One G]

/-- The unit of the multiplication is `single 1 1`, i.e. the function
that is `1` at `1` and zero elsewhere. -/
@[to_additive (dont_translate := k) one /--
The unit of the multiplication is `single 0 1`, i.e. the function
that is `1` at `0` and zero elsewhere. -/]
instance one : One (MonoidAlgebra k G) :=
  ⟨single 1 1⟩

@[to_additive (dont_translate := k) one_def]
theorem one_def : (1 : MonoidAlgebra k G) = single 1 1 :=
  rfl

end One

section MulOneClass

variable [Semiring k] [MulOneClass G]

@[to_additive (dont_translate := k)]
instance nonAssocSemiring : NonAssocSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalNonAssocSemiring with
    natCast := fun n => single 1 n
    natCast_zero := by simp
    natCast_succ := fun _ => by simp; rfl
    one_mul := fun f => by
      simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, one_mul,
        sum_single]
    mul_one := fun f => by
      simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, mul_one, sum_single] }

@[to_additive (dont_translate := k)]
theorem natCast_def (n : ℕ) : (n : MonoidAlgebra k G) = single (1 : G) (n : k) :=
  rfl

end MulOneClass

section SMul

/-! ### Basic scalar multiplication instances

This section collects instances needed for the algebraic structure of `Polynomial`,
which is defined in terms of `MonoidAlgebra`.
Further results on scalar multiplication can be found in
`Mathlib/Algebra/MonoidAlgebra/Module.lean`.
-/

variable {S : Type*}

@[to_additive smulZeroClass]
instance smulZeroClass [Semiring k] [SMulZeroClass R k] : SMulZeroClass R (MonoidAlgebra k G) :=
  Finsupp.smulZeroClass

@[to_additive distribSMul]
instance distribSMul [Semiring k] [DistribSMul R k] : DistribSMul R (MonoidAlgebra k G) :=
  Finsupp.distribSMul _ _

@[to_additive (dont_translate := R) isScalarTower]
instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S]
    [IsScalarTower R S k] : IsScalarTower R S (MonoidAlgebra k G) :=
  Finsupp.isScalarTower G k

@[to_additive (dont_translate := R) smulCommClass]
instance smulCommClass [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
    SMulCommClass R S (MonoidAlgebra k G) :=
  Finsupp.smulCommClass G k

@[to_additive (dont_translate := R) isCentralScalar]
instance isCentralScalar [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k]
    [IsCentralScalar R k] : IsCentralScalar R (MonoidAlgebra k G) :=
  Finsupp.isCentralScalar G k

end SMul

/-! #### Semiring structure -/


section Semiring

variable [Semiring k] [Monoid G]

@[to_additive]
instance semiring : Semiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalSemiring,
    MonoidAlgebra.nonAssocSemiring with }

variable [Semiring R]

@[to_additive (attr := simp, norm_cast)]
lemma coe_add (f g : MonoidAlgebra R G) : ⇑(f + g) = f + g := rfl

end Semiring

@[to_additive (dont_translate := k)]
instance nonUnitalCommSemiring [CommSemiring k] [CommSemigroup G] :
    NonUnitalCommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalSemiring with
    mul_comm := fun f g => by
      simp only [mul_def, Finsupp.sum, mul_comm]
      rw [Finset.sum_comm]
      simp only [mul_comm] }

@[to_additive]
instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (MonoidAlgebra k G) :=
  Finsupp.instNontrivial

/-! #### Derived instances -/


section DerivedInstances

@[to_additive]
instance commSemiring [CommSemiring k] [CommMonoid G] : CommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.semiring with }

@[to_additive]
instance unique [Semiring k] [Subsingleton k] : Unique (MonoidAlgebra k G) :=
  Finsupp.uniqueOfRight

@[to_additive addCommGroup]
instance addCommGroup [Ring k] : AddCommGroup (MonoidAlgebra k G) :=
  Finsupp.instAddCommGroup

@[to_additive]
instance nonUnitalNonAssocRing [Ring k] [Mul G] : NonUnitalNonAssocRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup, MonoidAlgebra.nonUnitalNonAssocSemiring with }

@[to_additive]
instance nonUnitalRing [Ring k] [Semigroup G] : NonUnitalRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup, MonoidAlgebra.nonUnitalSemiring with }

@[to_additive (dont_translate := k)]
instance nonAssocRing [Ring k] [MulOneClass G] : NonAssocRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup,
    MonoidAlgebra.nonAssocSemiring with
    intCast := fun z => single 1 (z : k)
    intCast_ofNat n := by simp [natCast_def]
    intCast_negSucc n := by simp [natCast_def, one_def] }

@[to_additive]
theorem intCast_def [Ring k] [MulOneClass G] (z : ℤ) :
    (z : MonoidAlgebra k G) = single (1 : G) (z : k) :=
  rfl

section Ring
variable [Ring R]

@[to_additive]
instance ring [Monoid G] : Ring (MonoidAlgebra R G) :=
  { MonoidAlgebra.nonAssocRing, MonoidAlgebra.semiring with }

@[to_additive]
lemma single_neg (a : M) (b : R) : single a (-b) = -single a b := Finsupp.single_neg ..

@[to_additive (attr := simp)]
lemma neg_apply (m : M) (x : MonoidAlgebra R M) : (-x) m = -x m := rfl

end Ring

@[to_additive]
instance nonUnitalCommRing [CommRing k] [CommSemigroup G] :
    NonUnitalCommRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.nonUnitalRing with }

@[to_additive]
instance commRing [CommRing k] [CommMonoid G] : CommRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommRing, MonoidAlgebra.ring with }

end DerivedInstances

@[to_additive (dont_translate := R) (attr := simp) smul_apply]
lemma smul_apply [Semiring S] [SMulZeroClass R S] (r : R) (m : M) (x : MonoidAlgebra S M) :
    (r • x) m = r • x m := rfl

@[to_additive (dont_translate := R) (attr := simp) smul_single]
theorem smul_single [Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) :
    c • single a b = single a (c • b) :=
  Finsupp.smul_single _ _ _

/-!
#### Copies of `ext` lemmas and bundled `single`s from `Finsupp`

As `MonoidAlgebra` is a type synonym, `ext` will not unfold it to find `ext` lemmas.
We need bundled version of `Finsupp.single` with the right types to state these lemmas.
It is good practice to have those, regardless of the `ext` issue.
-/

section ExtLemmas

/-- A copy of `Finsupp.ext` for `MonoidAlgebra`. -/
@[to_additive (attr := ext) /-- A copy of `Finsupp.ext` for `AddMonoidAlgebra`. -/]
theorem ext [Semiring k] ⦃f g : MonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) :
    f = g :=
  Finsupp.ext H

/-- A copy of `Finsupp.singleAddHom` for `MonoidAlgebra`. -/
@[to_additive /-- A copy of `Finsupp.singleAddHom` for `AddMonoidAlgebra`. -/]
abbrev singleAddHom [Semiring k] (a : G) : k →+ MonoidAlgebra k G := Finsupp.singleAddHom a

@[to_additive (attr := simp)]
lemma singleAddHom_apply [Semiring k] (a : G) (b : k) : singleAddHom a b = single a b := rfl

/-- A copy of `Finsupp.addHom_ext'` for `MonoidAlgebra`. -/
@[to_additive (attr := ext high) /-- A copy of `Finsupp.addHom_ext'` for `AddMonoidAlgebra`. -/]
theorem addHom_ext' {N : Type*} [Semiring k] [AddZeroClass N]
    ⦃f g : MonoidAlgebra k G →+ N⦄
    (H : ∀ (x : G), AddMonoidHom.comp f (singleAddHom x) = AddMonoidHom.comp g (singleAddHom x)) :
    f = g :=
  Finsupp.addHom_ext' H

end ExtLemmas

section MiscTheorems

variable [Semiring k]

@[to_additive (dont_translate := k) mul_apply]
theorem mul_apply [DecidableEq G] [Mul G] (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0 := by
  -- Porting note: `reducible` cannot be `local` so proof gets long.
  rw [mul_def, Finsupp.sum_apply]; congr; ext
  rw [Finsupp.sum_apply]; congr; ext
  apply single_apply

open Finset in
@[to_additive (dont_translate := k) mul_apply_antidiagonal]
theorem mul_apply_antidiagonal [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) : (f * g) x = ∑ p ∈ s, f p.1 * g p.2 := by
  classical exact
      let F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
      calc
        (f * g) x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := mul_apply f g x
        _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
        _ = ∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f p.1 * g p.2 :=
          (Finset.sum_filter _ _).symm
        _ = ∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f p.1 * g p.2 := by
          congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
        _ = ∑ p ∈ s, f p.1 * g p.2 :=
          sum_subset (filter_subset _ _) fun p hps hp => by
            simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
            by_cases h1 : f p.1 = 0
            · rw [h1, zero_mul]
            · rw [hp hps h1, mul_zero]

@[to_additive (dont_translate := k) (attr := simp) single_mul_single]
theorem single_mul_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
    single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) := by
  rw [mul_def]
  exact (sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
    (sum_single_index (by rw [mul_zero, single_zero]))

@[to_additive (dont_translate := k) single_commute_single]
theorem single_commute_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k}
    (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
    Commute (single a₁ b₁) (single a₂ b₂) :=
  single_mul_single.trans <| congr_arg₂ single ha hb |>.trans single_mul_single.symm

@[to_additive (dont_translate := k) single_commute]
theorem single_commute [Mul G] {a : G} {b : k} (ha : ∀ a', Commute a a') (hb : ∀ b', Commute b b') :
    ∀ f : MonoidAlgebra k G, Commute (single a b) f :=
  suffices AddMonoidHom.mulLeft (single a b) = AddMonoidHom.mulRight (single a b) from
    DFunLike.congr_fun this
  addHom_ext' fun a' => AddMonoidHom.ext fun b' => single_commute_single (ha a') (hb b')

@[to_additive (dont_translate := k) (attr := simp) single_pow]
theorem single_pow [Monoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (a ^ n) (b ^ n)
  | 0 => by
    simp only [pow_zero]
    rfl
  | n + 1 => by simp only [pow_succ, single_pow n, single_mul_single]

section

variable (k G)

/-- The embedding of a magma into its magma algebra. -/
@[simps]
def ofMagma [Mul G] : G →ₙ* MonoidAlgebra k G where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]

/-- The embedding of a unital magma into its magma algebra. -/
@[simps]
def of [MulOneClass G] : G →* MonoidAlgebra k G :=
  { ofMagma k G with
    toFun := fun a => single a 1
    map_one' := rfl }

end

theorem of_injective [MulOneClass G] [Nontrivial k] :
    Function.Injective (of k G) := fun a b h => by
  simpa using (single_eq_single_iff _ _ _ _).mp h

theorem of_commute [MulOneClass G] {a : G} (h : ∀ a', Commute a a') (f : MonoidAlgebra k G) :
    Commute (of k G a) f :=
  single_commute h Commute.one_left f

/-- `Finsupp.single` as a `MonoidHom` from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
-/
@[simps]
def singleHom [MulOneClass G] : k × G →* MonoidAlgebra k G where
  toFun a := single a.2 a.1
  map_one' := rfl
  map_mul' _a _b := single_mul_single.symm

@[to_additive (dont_translate := k) mul_single_apply_aux]
theorem mul_single_apply_aux [Mul G] (f : MonoidAlgebra k G) (r : k) {x y z : G}
    (H : ∀ a ∈ f.support, a * x = z ↔ a = y) : (f * single x r) z = f y * r := by
  classical exact
    calc
      (f * single x r) z
      _ = sum f fun a b => ite (a * x = z) (b * r) 0 :=
        (mul_apply _ _ _).trans <| Finsupp.sum_congr fun _ _ => sum_single_index (by simp)
      _ = f.sum fun a b => ite (a = y) (b * r) 0 := Finsupp.sum_congr fun x hx => by
        simp only [H _ hx]
      _ = if y ∈ f.support then f y * r else 0 := f.support.sum_ite_eq' _ _
      _ = _ := by split_ifs with h <;> simp at h <;> simp [h]

@[to_additive (dont_translate := k) mul_single_zero_apply]
theorem mul_single_one_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (HMul.hMul (β := MonoidAlgebra k G) f (single 1 r)) x = f x * r :=
  f.mul_single_apply_aux r fun a ha => by rw [mul_one]

@[to_additive (dont_translate := k) mul_single_apply_of_not_exists_add]
theorem mul_single_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
    (h : ¬∃ d, g' = d * g) : (x * single g r) g' = 0 := by
  classical
    rw [mul_apply, Finsupp.sum_comm, Finsupp.sum_single_index]
    swap
    · simp_rw [Finsupp.sum, mul_zero, ite_self, Finset.sum_const_zero]
    · apply Finset.sum_eq_zero
      grind

@[to_additive (dont_translate := k) single_mul_apply_aux]
theorem single_mul_apply_aux [Mul G] (f : MonoidAlgebra k G) (r : k) {x y z : G}
    (H : ∀ a ∈ f.support, x * a = y ↔ a = z) : (single x r * f) y = r * f z := by
  classical exact
      have : (f.sum fun a b => ite (x * a = y) (0 * b) 0) = 0 := by simp
      calc
        (single x r * f) y
        _ = sum f fun a b => ite (x * a = y) (r * b) 0 :=
          (mul_apply _ _ _).trans <| sum_single_index this
        _ = f.sum fun a b => ite (a = z) (r * b) 0 := Finsupp.sum_congr fun x hx => by
          simp only [H _ hx]
        _ = if z ∈ f.support then r * f z else 0 := f.support.sum_ite_eq' _ _
        _ = _ := by split_ifs with h <;> simp at h <;> simp [h]

@[to_additive (dont_translate := k) single_zero_mul_apply]
theorem single_one_mul_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (single (1 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux r fun a ha => by rw [one_mul]

@[to_additive (dont_translate := k) single_mul_apply_of_not_exists_add]
theorem single_mul_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
    (h : ¬∃ d, g' = g * d) : (single g r * x) g' = 0 := by
  classical
    rw [mul_apply, Finsupp.sum_single_index]
    swap
    · simp_rw [Finsupp.sum, zero_mul, ite_self, Finset.sum_const_zero]
    · apply Finset.sum_eq_zero
      grind

end MiscTheorems

@[to_additive (dont_translate := k)]
theorem single_one_comm [CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) :
    single (1 : G) r * f = f * single (1 : G) r :=
  single_commute Commute.one_left (Commute.all _) f

/-- `Finsupp.single 1` as a `RingHom` -/
@[to_additive (dont_translate := k) (attr := simps) /-- `Finsupp.single 0` as a `RingHom` -/]
def singleOneRingHom [Semiring k] [MulOneClass G] : k →+* MonoidAlgebra k G :=
  { singleAddHom 1 with
    toFun := single 1
    map_one' := rfl
    map_mul' := fun x y => by simp }

/-- If two ring homomorphisms from `MonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal. -/
@[to_additive (dont_translate := R k)]
theorem ringHom_ext {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
    (h₁ : ∀ b, f (single 1 b) = g (single 1 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) :
    f = g :=
  RingHom.coe_addMonoidHom_injective <|
    addHom_ext fun a b => by
      rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single]
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g]; rw [f.map_mul, g.map_mul, h₁, h_of]

/-- If two ring homomorphisms from `MonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
    (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
    (h_of :
      (f : MonoidAlgebra k G →* R).comp (of k G) = (g : MonoidAlgebra k G →* R).comp (of k G)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

theorem induction_on [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G)
    (hM : ∀ g, p (of k G g)) (hadd : ∀ f g : MonoidAlgebra k G, p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f := by
  refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_
  · simpa using hsmul 0 (of k G 1) (hM 1)
  · convert hsmul r (of k G g) (hM g)
    simp

section

universe ui

variable {ι : Type ui}

open Finset in
@[to_additive (dont_translate := k) prod_single]
theorem prod_single [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i ∈ s, single (a i) (b i)) = single (∏ i ∈ s, a i) (∏ i ∈ s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, prod_cons has, prod_cons has]

end

section

-- We now prove some additional statements that hold for group algebras.
variable [Semiring k] [Group G]

@[to_additive (dont_translate := k) (attr := simp) mul_single_apply]
theorem mul_single_apply (f : MonoidAlgebra k G) (r : k) (x y : G) :
    (f * single x r) y = f (y * x⁻¹) * r :=
  f.mul_single_apply_aux r fun _a _ => eq_mul_inv_iff_mul_eq.symm

@[to_additive (dont_translate := k) (attr := simp) single_mul_apply]
theorem single_mul_apply (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) :
    (single x r * f) y = r * f (x⁻¹ * y) :=
  f.single_mul_apply_aux r fun _z _ => eq_inv_mul_iff_mul_eq.symm

@[to_additive (dont_translate := k) mul_apply_left]
theorem mul_apply_left (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a b => b * g (a⁻¹ * x) :=
  calc
    (f * g) x = sum f fun a b => (single a b * g) x := by
      rw [← Finsupp.sum_apply, ← Finsupp.sum_mul g f, f.sum_single]
    _ = _ := by simp only [single_mul_apply, Finsupp.sum]

-- If we'd assumed `CommSemiring`, we could deduce this from `mul_apply_left`.
@[to_additive (dont_translate := k) mul_apply_right]
theorem mul_apply_right (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = g.sum fun a b => f (x * a⁻¹) * b :=
  calc
    (f * g) x = sum g fun a b => (f * single a b) x := by
      rw [← Finsupp.sum_apply, ← Finsupp.mul_sum f g, g.sum_single]
    _ = _ := by simp only [mul_single_apply, Finsupp.sum]

end

@[to_additive (dont_translate := k)]
instance isLocalHom_singleOneRingHom [Semiring k] [Monoid G] :
    IsLocalHom (singleOneRingHom (k := k) (G := G)) where
  map_nonunit x hx := by
    obtain ⟨⟨x, xi, hx, hxi⟩, rfl⟩ := hx
    simp_rw [MonoidAlgebra.ext_iff, singleOneRingHom_apply] at hx hxi ⊢
    specialize hx 1
    specialize hxi 1
    classical
    simp_rw [single_one_mul_apply, one_def, single_apply, if_pos] at hx
    simp_rw [mul_single_one_apply, one_def, single_apply, if_pos] at hxi
    exact ⟨⟨x, xi 1, hx, hxi⟩, rfl⟩

end MonoidAlgebra

/-! ### Additive monoids -/


namespace AddMonoidAlgebra

variable {k G}

section MiscTheorems

variable [Semiring k]

section

variable (k G)

/-- The embedding of an additive magma into its additive magma algebra. -/
@[simps]
def ofMagma [Add G] : Multiplicative G →ₙ* k[G] where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]; rfl

/-- Embedding of a magma with zero into its magma algebra. -/
def of [AddZeroClass G] : Multiplicative G →* k[G] :=
  { ofMagma k G with
    toFun := fun a => single a 1
    map_one' := rfl }

/-- Embedding of a magma with zero `G`, into its magma algebra, having `G` as source. -/
def of' : G → k[G] := fun a => single a 1

end

@[simp]
theorem of_apply [AddZeroClass G] (a : Multiplicative G) :
    of k G a = single a.toAdd 1 :=
  rfl

@[simp]
theorem of'_apply (a : G) : of' k G a = single a 1 :=
  rfl

theorem of'_eq_of [AddZeroClass G] (a : G) : of' k G a = of k G (.ofAdd a) := rfl

theorem of_injective [Nontrivial k] [AddZeroClass G] : Function.Injective (of k G) :=
  MonoidAlgebra.of_injective

theorem of'_commute [AddZeroClass G] {a : G} (h : ∀ a', AddCommute a a')
    (f : AddMonoidAlgebra k G) :
    Commute (of' k G a) f :=
  MonoidAlgebra.of_commute (G := Multiplicative G) h f

/-- `Finsupp.single` as a `MonoidHom` from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
-/
@[simps]
def singleHom [AddZeroClass G] : k × Multiplicative G →* k[G] where
  toFun a := single a.2.toAdd a.1
  map_one' := rfl
  map_mul' _a _b := single_mul_single.symm

/-- Copy of `Finsupp.smul_single'` that avoids the `AddMonoidAlgebra = Finsupp` defeq abuse. -/
theorem smul_single' (c : k) (a : G) (b : k) : c • single a b = single a (c * b) :=
  Finsupp.smul_single' c a b

theorem induction_on [AddMonoid G] {p : k[G] → Prop} (f : k[G])
    (hM : ∀ g, p (of k G (Multiplicative.ofAdd g)))
    (hadd : ∀ f g : k[G], p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f := by
  refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_
  · simpa using hsmul 0 (of k G (Multiplicative.ofAdd 0)) (hM 0)
  · convert hsmul r (of k G (Multiplicative.ofAdd g)) (hM g)
    simp

end MiscTheorems

/-! #### Algebra structure -/

/-- If two ring homomorphisms from `k[G]` are equal on all `single a 1`
and `single 0 b`, then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G] →+* R}
    (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom)
    (h_of : (f : k[G] →* R).comp (of k G) = (g : k[G] →* R).comp (of k G)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

end AddMonoidAlgebra
